Date: Tue, 14 Jan 1997 20:33:41 GMT
Server: Apache/1.0.3
Content-type: text/html
Content-length: 7757
Last-modified: Wed, 04 Dec 1996 00:47:34 GMT

<HTML>
<HEAD>
<TITLE>Home Page for Paul E. Black</TITLE>
<!-- describe the document, avoid context sensitive descriptions -->
<meta name="description" 
      value="Biographical information about Paul Black with links to 
		on-line copies of technical reports.">

<!-- keywords for the document -->
<meta name="keywords"
     value="HOL, theorem proving, BYU">

<!-- should be "document" unless providing a search, then "service" -->
<meta name="resource-type" 
      value="document">

<!-- use global for documents to be indexed outside BYU -->
<meta name="distribution" value="global">

</HEAD>
<BODY>

<h1>Home Page for Paul E. Black</h1>


<ADDRESS>Paul E. Black</ADDRESS>
<ADDRESS>
<!WA0><A HREF="http://lal.cs.byu.edu/homepage.html">Laboratory for Applied Logic</A>
</ADDRESS>        
<ADDRESS>
<!WA1><A HREF="http://www.cs.byu.edu/">Dept. of Computer Science</A>, 
<!WA2><A HREF="http://www.cs.byu.edu/building/TMCB-3rd.html">TMCB 3325</A>
</ADDRESS>
<ADDRESS>
<!WA3><A HREF="http://www.byu.edu/">Brigham Young University</A>
</ADDRESS>
<ADDRESS>
<!WA4><A HREF="http://www.cs.byu.edu/map-info/tourProvo.html">Provo</A>,
<!WA5><A HREF="http://www.cs.byu.edu/tourUtah.html">Utah</A>
       84602-6576
</ADDRESS>
<P>

<ADDRESS><!WA6><img align=top src="http://lal.cs.byu.edu/images/phone-small.xbm" alt="telephone:"> 
  +1 801 378 8113</ADDRESS>  
<ADDRESS>black@cs.byu.edu</ADDRESS>
<ADDRESS>p.black@ieee.org</ADDRESS>
<ADDRESS>KC7PKT</ADDRESS>

<P>
Paul Black is studying at
<!WA7><A HREF="http://www.byu.edu/">Brigham Young University</A>
where he is pursuing a Ph.D. in Computer Science.  He began his Ph.D.
program at 
<!WA8><A HREF="http://www.berkeley.edu/">UC Berkeley</A>, and
transferred to BYU in 1993.  His research interests are
formal verification of software and software engineering.

<P>
Black earned an MS in Computer Science at the 
<!WA9><A HREF="http://www.cs.utah.edu/">University of Utah</A>
in 1983 and a BS in Mathematics at 
<!WA10><A HREF="http://www.suu.edu/">Southern Utah State College</A> (now
Southern Utah University) in 1973.  He
has 17 years industrial experience developing IC design and
verification tools, designing configuration management systems,
assuring software quality, and managing business data processing.  He
is a student member of the <!WA11><A HREF="http://info.acm.org">ACM</A> and
the <!WA12><A HREF="http://www.ieee.org/">IEEE</A>. 

<P>
He served a mission for the
<!WA13><A HREF="http://www.lds.org/">LDS Church</a> in
<!WA14><A HREF="http://www.xmission.com/~dkenison/brasil/bra_sps.html">Brazil</A>, 
and has visited 
<!WA15><A HREF="http://www.adfa.oz.au/CS/flg/col/be.html">Belgium</A>, 
<!WA16><A HREF="http://www.adfa.oz.au/CS/flg/col/ca.html">Canada</A>, 
<!WA17><A HREF="http://www.vn.fi/vn/um/">Finland</A>,
<!WA18><A HREF="http://www.adfa.oz.au/CS/flg/col/de.html">Germany</A>, 
<!WA19><A HREF="http://www.adfa.oz.au/CS/flg/col/gb.html">Great Britain</A>, and 
<!WA20><A HREF="http://www.adfa.oz.au/CS/flg/col/mx.html">Mexico</A>.
There's even a recent 
<!WA21><A HREF="http://lal.cs.byu.edu/pictures/Paul.Black.gif">picture</A> on-line.
He keeps favorite links in a
<!WA22><A HREF="http://lal.cs.byu.edu/people/black/hotlist.html">personal hotlist</A>
which he updates occasionally.

<HR>

<H2>Published Papers On-Line</H2>

<UL>
<LI>
<strong>Paul E. Black and Phillip J. Windley</strong>,
<em>Verifying Resilient Software</em>,
to be printed in the Proceedings of the
<!WA23><A HREF="http://www.cba.hawaii.edu/hicss/">
Thirtieth Hawai`i International Conference on on System Sciences
(HICSS-30)</A>, January 1997.
<!WA24><A HREF="http://lal.cs.byu.edu/people/black/Papers/hicss30.dvi">
DVI</A> (36 kb) and
<!WA25><A HREF="http://lal.cs.byu.edu/people/black/Papers/hicss30.ps">
Postscript</A> (123 kb).

<LI>
<strong>Paul E. Black and Phillip J. Windley</strong>,
<em>Inference Rules for Programming Languages with Side Effects in
Expressions</em>,
<!WA26><A HREF="http://www.abo.fi/~jharriso/TPHOLs96.html">
Theorem Proving in Higher Order Logics:
9th International Conference, (TPHOLs '96)</A>,
edited by Joakim von Wright, Jim Grundy, and John Harrison,
Springer-Verlag, Berlin, Germany, 1996, pp. 51-60.
<!WA27><A HREF="http://lal.cs.byu.edu/people/black/Papers/hol96.dvi">
DVI</A> (34 kb) and
<!WA28><A HREF="http://lal.cs.byu.edu/people/black/Papers/hol96.ps">
Postscript</A> (128 kb).

<LI>
<strong>Paul E. Black, Kelly M. Hall, Michael D. Jones, Trent
N. Larson, and Phillip J. Windley</strong>, 
<em>A Brief Introduction to Formal Methods</em>,
Proceedings of the IEEE 1996 Custom Integrated Circuits Conference, San
Diego, California, May 1996. 
<!WA29><A HREF="http://lal.cs.byu.edu/people/black/Papers/formMeth.ps">
Postscript</A> (96 kb).

<LI>
<strong>Paul E. Black and Phillip J. Windley</strong>,
<em>Automatically Synthesized Term Denotation Predicates: A Proof Aid</em>,
<!WA30><A HREF="http://lal.cs.byu.edu/lal/hol95/hol95.html">
Higher Order Logic Theorem Proving and Its Applications (HOL '95)</A>, 
edited by E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss,
Springer-Verlag, Berlin, Germany, 1995, pp. 46-57.
<!WA31><A HREF="http://lal.cs.byu.edu/people/black/Papers/hol95.ps">
Postscript</A> (120 kb).

<LI>
<strong>Mor Harchol-Balter and Paul E. Black</strong>,
<em>Queuing Analysis of Oblivious Packet-Routing Networks</em>,
5th ACM/<!WA32><A HREF="http://www.siam.org/">SIAM</a> Symposium on Discrete
Algorithms (SODA '94), Washington, D.C., (January 1994), ACM, pp. 583 - 592. 
<!WA33><A HREF="http://lal.cs.byu.edu/people/black/Papers/soda.ps">
Postscript</A> (190 kb).  Expanded version with application to tori in
<!WA34><A HREF="http://lal.cs.byu.edu/people/black/Papers/extension.ps">
Postscript</A> (203 kb).

</UL>

<H2>Finished Projects</H2>

<UL>
<LI>I taught <!WA35><A HREF="http://lal.cs.byu.edu/cs130">Scientific
Programming - C</a>.

<LI>
Notes on my lecture to the Software Engineering course on
<!WA36><a href="http://lal.cs.byu.edu/people/black/cs327.chap9.html">
Formal Methods</a>

<LI><!WA37><A HREF="http://lal.cs.byu.edu/people/black/universe.html">On the
Composition of the Universe</A>

<LI>The Orbiter
<!WA38><A HREF="http://lal.cs.byu.edu/people/black/shuttle.html">Discovery's
Visit to Utah</A>.

</UL>

<H3>Other, Less Directed Links</H3>

<P>
I've put together some web sites and collections.  Here
are some I'm especially happy with and links to other miscellaneous
on-line stuff of mine.

<UL>
<LI>
The
<!WA39><A HREF="http://lal.cs.byu.edu/people/black/dickinson.html">
Emily Dickinson home page</A> including an
<!WA40><A HREF="http://lal.cs.byu.edu/mlists/emweb/">
archive of a discussion list</A> and links to over
<!WA41><A HREF="http://lal.cs.byu.edu/people/EDickinson/poemsOnline.html">370 of her poems on-line</a>.

<LI>
I led a group consisting of most of my OO class in building a hypertext
<!WA42><A HREF="http://osm7.cs.byu.edu/OSA/tutorial.html">
OSA Tutorial</A>.  There are 
<!WA43><A HREF="http://osm7.cs.byu.edu/OSA/generalConst.html#beSpecific">
links to on-line quizes</A>, but the quiz program is currently
(21Mar96) not working.

<LI>
As an experiment in HTML graphics and interfaces, I designed some
pages to resemble
<!WA44><A HREF="http://www.imall.com/startrek/ncc1701d/">
control panels on the Enterprise</a>.

<LI>
To help a professor, I put the
<!WA45><A HREF="http://lal.cs.byu.edu/lalac/">
Language And Learning Across Curriculum</A> Committee on line,
converting their
<!WA46><A HREF="http://lal.cs.byu.edu/lalac/bibliog.html">bibliography</a>,
<!WA47><A HREF="http://lal.cs.byu.edu/lalac/brochure.html">brochure</a>,
etc. to HTML.

<LI>
Learning HOL lessons.
<!WA48><A HREF="http://lal.cs.byu.edu/people/black/lesson1.html">
Goal Directed Proof</A> (#1),
<!WA49><A HREF="http://lal.cs.byu.edu/people/black/lesson2.html">
Induction</A> (#2),
<!WA50><A HREF="http://lal.cs.byu.edu/people/black/lesson4.html">
The Assumption List</A> (#4).

</UL>

<HR>

<EM>Updated
Tue Dec  3 17:47:33 1996
</EM><ADDRESS>
by <!WA51><a href="http://lal.cs.byu.edu/people/black/black.html">Paul E. Black
</a>
&nbsp;(<!WA52><a href="mailto:black@lal.cs.byu.edu">black@lal.cs.byu.edu</a>)
</ADDRESS>
</BODY>
</HTML>
